FDL - Nuprl Lemma : combine-causally-related

Nuprl Lemma : combine-causally-related

es:ES, A, B, P, Q:(E

), T, T':Type, R:(T

T'

).
(

e:E. (A(e)

B(e))

(valtype(e)

r T))

(

e:E. (P(e)

Q(e))

(valtype(e)

r T'))

(e.A(e)

e.P(e)) with R

(e.B(e)

e.Q(e)) with R

(

e:E.

(A(e) & B(e)))

(

e:E.

(P(e) & Q(e)))

(

e:E. Dec(P(e)))

(

e:E. Dec(A(e)))

(e.A(e)

B(e)

e.P(e)

Q(e)) with R

Definitions x:A. B(x), {T}, x. t(x), t T, P & Q, (e.P(e) e'.Q(e')) with R, x(s), P Q, P Q, , x:A. B(x)

Lemmas causal-bijection wf, combine-causal-bijections, event system wf, es-valtype wf, causally-related wf, not wf, decidable wf, es-E wf